Nuprl Lemma : R-interface-compat-self
0,22
postcript
pdf
A
:Realizer. R-Feasible(
A
)
R-interface-compat(
A
;
A
)
latex
Definitions
t
T
,
P
Q
,
x
:
A
.
B
(
x
)
,
R-self-interface(
R
)
,
Realizer
,
R-Feasible(
R
)
,
R-interface-compat(
A
;
B
)
Lemmas
R-Feasible
wf
,
es
realizer
wf
,
R-self-interface-implies
,
R-Feasible-self-interface
origin
A:Realizer. R-Feasible(A) 
R-interface-compat(A;A) A:Realizer. R-Feasible(A) R-interface-compat(A;A) 
T Qx:A. B(x)